package com.googlecode.kipler.transformations;

import com.googlecode.kipler.syntax.formula.BooleanFormula;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.ConceptDefinition;
import com.googlecode.kipler.syntax.formula.Formula;
import com.googlecode.kipler.syntax.formula.FormulaVisitor;
import com.googlecode.kipler.syntax.formula.LTLBinaryFormula;
import com.googlecode.kipler.syntax.formula.LTLUnaryFormula;
import com.googlecode.kipler.syntax.formula.ObjectRoleAssertion;
import com.googlecode.kipler.syntax.formula.RoleAssertion;
import com.googlecode.kipler.syntax.formula.RoleInclusion;
import com.googlecode.kipler.syntax.formula.SameIndividualAssertion;


/**
 * 
 * @author İnanç Seylan
 * 
 */
public class FormulaSimplificationVisitor implements FormulaVisitor {
	private Formula normalForm;

	public Formula getNormalForm() {
		return normalForm;
	}

	public void visitBooleanFormula(BooleanFormula be) {
		normalForm = be;
		FormulaSimplificationVisitor visitor = new FormulaSimplificationVisitor();
		be.getLhs().accept(visitor);
		be.setLhs(visitor.getNormalForm());
		visitor = new FormulaSimplificationVisitor();
		be.getRhs().accept(visitor);
		be.setRhs(visitor.getNormalForm());
	}

	public void visitConceptAssertion(ConceptAssertion ca) {
		normalForm = ca;
		ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
		ca.getConcept().accept(visitor);
		ca.setConcept(visitor.getNormalForm());
	}

	public void visitConceptDefinition(ConceptDefinition cd) {
		normalForm = cd;
		ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
		cd.getLhs().accept(visitor);
		cd.setLhs(visitor.getNormalForm());
		visitor = new ConceptSimplificationVisitor();
		cd.getRhs().accept(visitor);
		cd.setRhs(visitor.getNormalForm());
	}

	public void visitObjectRoleAssertion(ObjectRoleAssertion ra) {
		normalForm = ra;
	}

	public void visitRoleAssertion(RoleAssertion ra) {
		normalForm = ra;
	}

	public void visitRoleInclusion(RoleInclusion ri) {
		normalForm = ri;
	}

	public void visitSameIndividualAssertion(SameIndividualAssertion ia) {
		normalForm = ia;
	}

	@Override
	public void visitLTLUnaryFormula(LTLUnaryFormula unFor) {
		normalForm = unFor;
		FormulaSimplificationVisitor visitor = new FormulaSimplificationVisitor();
		unFor.getOperand().accept(visitor);
		unFor.setOperand(visitor.getNormalForm());
	}

	@Override
	public void visitLTLBinaryFormula(LTLBinaryFormula binFor) {
		normalForm = binFor;
		FormulaSimplificationVisitor visitor = new FormulaSimplificationVisitor();
		binFor.getLhs().accept(visitor);
		binFor.setLhs(visitor.getNormalForm());
		visitor = new FormulaSimplificationVisitor();
		binFor.getRhs().accept(visitor);
		binFor.setRhs(visitor.getNormalForm());
	}

}
